(set-logic QF_ABV)
(set-info :source |
This benchmark comes from bounded model checking of two fifo implementations.
The fifos are resetted once at the beginning.
We try to verify behavioral equivalence with k-induction.
All different constraints are used on registers
and also on arrays that model internal memory respectively.
Fifo inputs: 'enqueue', 'dequeue', 'reset' (active low) and 'data_in'.
Fifo output: 'empty', 'full' and 'data_out'.
Bit-width: 32
k: 5
The fifos have an internal memory of size 64, respectively modelled as array.

Contributed by Robert Brummayer (robert.brummayer@gmail.com).
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status sat)
(declare-fun head_fs_0 () (_ BitVec 6))
(declare-fun tail_fs_0 () (_ BitVec 6))
(declare-fun full_fs_0 () (_ BitVec 1))
(declare-fun empty_fs_0 () (_ BitVec 1))
(declare-fun data_out_fs_0 () (_ BitVec 32))
(declare-fun head_fq_0 () (_ BitVec 6))
(declare-fun tail_fq_0 () (_ BitVec 6))
(declare-fun full_fq_0 () (_ BitVec 1))
(declare-fun empty_fq_0 () (_ BitVec 1))
(declare-fun data_out_fq_0 () (_ BitVec 32))
(declare-fun reset_0 () (_ BitVec 1))
(declare-fun a88 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun a89 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun enqeue_0 () (_ BitVec 1))
(declare-fun deqeue_0 () (_ BitVec 1))
(declare-fun data_in_0 () (_ BitVec 32))
(declare-fun head_fs_1 () (_ BitVec 6))
(declare-fun tail_fs_1 () (_ BitVec 6))
(declare-fun full_fs_1 () (_ BitVec 1))
(declare-fun empty_fs_1 () (_ BitVec 1))
(declare-fun data_out_fs_1 () (_ BitVec 32))
(declare-fun head_fq_1 () (_ BitVec 6))
(declare-fun tail_fq_1 () (_ BitVec 6))
(declare-fun full_fq_1 () (_ BitVec 1))
(declare-fun empty_fq_1 () (_ BitVec 1))
(declare-fun data_out_fq_1 () (_ BitVec 32))
(declare-fun reset_1 () (_ BitVec 1))
(declare-fun a305 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun a307 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun enqeue_1 () (_ BitVec 1))
(declare-fun deqeue_1 () (_ BitVec 1))
(declare-fun data_in_1 () (_ BitVec 32))
(declare-fun head_fs_2 () (_ BitVec 6))
(declare-fun tail_fs_2 () (_ BitVec 6))
(declare-fun full_fs_2 () (_ BitVec 1))
(declare-fun empty_fs_2 () (_ BitVec 1))
(declare-fun data_out_fs_2 () (_ BitVec 32))
(declare-fun head_fq_2 () (_ BitVec 6))
(declare-fun tail_fq_2 () (_ BitVec 6))
(declare-fun full_fq_2 () (_ BitVec 1))
(declare-fun empty_fq_2 () (_ BitVec 1))
(declare-fun data_out_fq_2 () (_ BitVec 32))
(declare-fun reset_2 () (_ BitVec 1))
(declare-fun a539 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun a543 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun enqeue_2 () (_ BitVec 1))
(declare-fun deqeue_2 () (_ BitVec 1))
(declare-fun data_in_2 () (_ BitVec 32))
(declare-fun head_fs_3 () (_ BitVec 6))
(declare-fun tail_fs_3 () (_ BitVec 6))
(declare-fun full_fs_3 () (_ BitVec 1))
(declare-fun empty_fs_3 () (_ BitVec 1))
(declare-fun data_out_fs_3 () (_ BitVec 32))
(declare-fun head_fq_3 () (_ BitVec 6))
(declare-fun tail_fq_3 () (_ BitVec 6))
(declare-fun full_fq_3 () (_ BitVec 1))
(declare-fun empty_fq_3 () (_ BitVec 1))
(declare-fun data_out_fq_3 () (_ BitVec 32))
(declare-fun reset_3 () (_ BitVec 1))
(declare-fun a779 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun a785 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun enqeue_3 () (_ BitVec 1))
(declare-fun deqeue_3 () (_ BitVec 1))
(declare-fun data_in_3 () (_ BitVec 32))
(declare-fun head_fs_4 () (_ BitVec 6))
(declare-fun tail_fs_4 () (_ BitVec 6))
(declare-fun full_fs_4 () (_ BitVec 1))
(declare-fun empty_fs_4 () (_ BitVec 1))
(declare-fun data_out_fs_4 () (_ BitVec 32))
(declare-fun head_fq_4 () (_ BitVec 6))
(declare-fun tail_fq_4 () (_ BitVec 6))
(declare-fun full_fq_4 () (_ BitVec 1))
(declare-fun empty_fq_4 () (_ BitVec 1))
(declare-fun data_out_fq_4 () (_ BitVec 32))
(declare-fun reset_4 () (_ BitVec 1))
(declare-fun a1025 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun a1033 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun enqeue_4 () (_ BitVec 1))
(declare-fun deqeue_4 () (_ BitVec 1))
(declare-fun data_in_4 () (_ BitVec 32))
(declare-fun head_fs_5 () (_ BitVec 6))
(declare-fun tail_fs_5 () (_ BitVec 6))
(declare-fun full_fs_5 () (_ BitVec 1))
(declare-fun empty_fs_5 () (_ BitVec 1))
(declare-fun data_out_fs_5 () (_ BitVec 32))
(declare-fun head_fq_5 () (_ BitVec 6))
(declare-fun tail_fq_5 () (_ BitVec 6))
(declare-fun full_fq_5 () (_ BitVec 1))
(declare-fun empty_fq_5 () (_ BitVec 1))
(declare-fun data_out_fq_5 () (_ BitVec 32))
(declare-fun reset_5 () (_ BitVec 1))
(declare-fun a1277 () (Array (_ BitVec 6) (_ BitVec 32)))
(declare-fun a1287 () (Array (_ BitVec 6) (_ BitVec 32)))
(assert (let ((?v_17 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_0 tail_fs_0) full_fs_0) empty_fs_0) data_out_fs_0) head_fq_0) tail_fq_0) full_fq_0) empty_fq_0) data_out_fq_0) reset_0)) (?v_45 (= (_ bv1 1) full_fs_0)) (?v_40 (= (_ bv1 1) enqeue_0)) (?v_39 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_0) (bvnot deqeue_0))) (bvnot (bvand enqeue_0 deqeue_0))))) (?v_38 (= (_ bv1 1) reset_0)) (?v_43 (= (_ bv1 1) deqeue_0)) (?v_44 (bvadd (_ bv1 6) head_fq_0)) (?v_42 (bvadd (_ bv1 6) tail_fq_0)) (?v_41 (= (_ bv1 1) full_fq_0)) (?v_19 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_1 tail_fs_1) full_fs_1) empty_fs_1) data_out_fs_1) head_fq_1) tail_fq_1) full_fq_1) empty_fq_1) data_out_fq_1) reset_1)) (?v_37 (= (_ bv1 1) full_fs_1)) (?v_32 (= (_ bv1 1) enqeue_1)) (?v_31 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_1) (bvnot deqeue_1))) (bvnot (bvand enqeue_1 deqeue_1))))) (?v_30 (= (_ bv1 1) reset_1)) (?v_35 (= (_ bv1 1) deqeue_1)) (?v_36 (bvadd (_ bv1 6) head_fq_1)) (?v_34 (bvadd (_ bv1 6) tail_fq_1)) (?v_33 (= (_ bv1 1) full_fq_1)) (?v_20 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_2 tail_fs_2) full_fs_2) empty_fs_2) data_out_fs_2) head_fq_2) tail_fq_2) full_fq_2) empty_fq_2) data_out_fq_2) reset_2)) (?v_29 (= (_ bv1 1) full_fs_2)) (?v_24 (= (_ bv1 1) enqeue_2)) (?v_23 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_2) (bvnot deqeue_2))) (bvnot (bvand enqeue_2 deqeue_2))))) (?v_22 (= (_ bv1 1) reset_2)) (?v_27 (= (_ bv1 1) deqeue_2)) (?v_28 (bvadd (_ bv1 6) head_fq_2)) (?v_26 (bvadd (_ bv1 6) tail_fq_2)) (?v_25 (= (_ bv1 1) full_fq_2)) (?v_21 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_3 tail_fs_3) full_fs_3) empty_fs_3) data_out_fs_3) head_fq_3) tail_fq_3) full_fq_3) empty_fq_3) data_out_fq_3) reset_3)) (?v_16 (= (_ bv1 1) full_fs_3)) (?v_11 (= (_ bv1 1) enqeue_3)) (?v_10 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_3) (bvnot deqeue_3))) (bvnot (bvand enqeue_3 deqeue_3))))) (?v_9 (= (_ bv1 1) reset_3)) (?v_14 (= (_ bv1 1) deqeue_3)) (?v_15 (bvadd (_ bv1 6) head_fq_3)) (?v_13 (bvadd (_ bv1 6) tail_fq_3)) (?v_12 (= (_ bv1 1) full_fq_3)) (?v_18 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_4 tail_fs_4) full_fs_4) empty_fs_4) data_out_fs_4) head_fq_4) tail_fq_4) full_fq_4) empty_fq_4) data_out_fq_4) reset_4)) (?v_7 (= (_ bv1 1) full_fs_4)) (?v_2 (= (_ bv1 1) enqeue_4)) (?v_1 (= (_ bv1 1) (bvand (bvnot (bvand (bvnot enqeue_4) (bvnot deqeue_4))) (bvnot (bvand enqeue_4 deqeue_4))))) (?v_0 (= (_ bv1 1) reset_4)) (?v_5 (= (_ bv1 1) deqeue_4)) (?v_6 (bvadd (_ bv1 6) head_fq_4)) (?v_4 (bvadd (_ bv1 6) tail_fq_4)) (?v_3 (= (_ bv1 1) full_fq_4)) (?v_8 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat head_fs_5 tail_fs_5) full_fs_5) empty_fs_5) data_out_fs_5) head_fq_5) tail_fq_5) full_fq_5) empty_fq_5) data_out_fq_5) reset_5))) (not (= (bvand reset_5 (bvand (bvnot (bvand (ite (= data_out_fs_5 data_out_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_5 full_fq_5) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_5 empty_fq_5) (_ bv1 1) (_ bv0 1))))) (bvand reset_5 (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_2 (ite ?v_3 a1033 (store a1033 tail_fq_4 data_in_4)) a1033) a1033) a1033) a1287) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_4) deqeue_4)) (select a1033 head_fq_4) data_out_fq_4) data_out_fq_4) data_out_fq_4) data_out_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_2 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_4 ?v_6) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_4)) empty_fq_4) (_ bv1 1)) empty_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_5 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_4 (bvadd (_ bv1 6) ?v_4)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_4)) full_fq_4) (_ bv0 1)) full_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_2 (ite ?v_3 tail_fq_4 ?v_4) tail_fq_4) tail_fq_4) (_ bv0 6)) tail_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_5 (ite (= (_ bv1 1) empty_fq_4) head_fq_4 ?v_6) head_fq_4) head_fq_4) (_ bv0 6)) head_fq_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_2 (ite ?v_7 a1025 (store a1025 tail_fs_4 data_in_4)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a1025 (_ bv0 6) (select a1025 (_ bv1 6))) (_ bv1 6) (select a1025 (_ bv2 6))) (_ bv2 6) (select a1025 (_ bv3 6))) (_ bv3 6) (select a1025 (_ bv4 6))) (_ bv4 6) (select a1025 (_ bv5 6))) (_ bv5 6) (select a1025 (_ bv6 6))) (_ bv6 6) (select a1025 (_ bv7 6))) (_ bv7 6) (select a1025 (_ bv8 6))) (_ bv8 6) (select a1025 (_ bv9 6))) (_ bv9 6) (select a1025 (_ bv10 6))) (_ bv10 6) (select a1025 (_ bv11 6))) (_ bv11 6) (select a1025 (_ bv12 6))) (_ bv12 6) (select a1025 (_ bv13 6))) (_ bv13 6) (select a1025 (_ bv14 6))) (_ bv14 6) (select a1025 (_ bv15 6))) (_ bv15 6) (select a1025 (_ bv16 6))) (_ bv16 6) (select a1025 (_ bv17 6))) (_ bv17 6) (select a1025 (_ bv18 6))) (_ bv18 6) (select a1025 (_ bv19 6))) (_ bv19 6) (select a1025 (_ bv20 6))) (_ bv20 6) (select a1025 (_ bv21 6))) (_ bv21 6) (select a1025 (_ bv22 6))) (_ bv22 6) (select a1025 (_ bv23 6))) (_ bv23 6) (select a1025 (_ bv24 6))) (_ bv24 6) (select a1025 (_ bv25 6))) (_ bv25 6) (select a1025 (_ bv26 6))) (_ bv26 6) (select a1025 (_ bv27 6))) (_ bv27 6) (select a1025 (_ bv28 6))) (_ bv28 6) (select a1025 (_ bv29 6))) (_ bv29 6) (select a1025 (_ bv30 6))) (_ bv30 6) (select a1025 (_ bv31 6))) (_ bv31 6) (select a1025 (_ bv32 6))) (_ bv32 6) (select a1025 (_ bv33 6))) (_ bv33 6) (select a1025 (_ bv34 6))) (_ bv34 6) (select a1025 (_ bv35 6))) (_ bv35 6) (select a1025 (_ bv36 6))) (_ bv36 6) (select a1025 (_ bv37 6))) (_ bv37 6) (select a1025 (_ bv38 6))) (_ bv38 6) (select a1025 (_ bv39 6))) (_ bv39 6) (select a1025 (_ bv40 6))) (_ bv40 6) (select a1025 (_ bv41 6))) (_ bv41 6) (select a1025 (_ bv42 6))) (_ bv42 6) (select a1025 (_ bv43 6))) (_ bv43 6) (select a1025 (_ bv44 6))) (_ bv44 6) (select a1025 (_ bv45 6))) (_ bv45 6) (select a1025 (_ bv46 6))) (_ bv46 6) (select a1025 (_ bv47 6))) (_ bv47 6) (select a1025 (_ bv48 6))) (_ bv48 6) (select a1025 (_ bv49 6))) (_ bv49 6) (select a1025 (_ bv50 6))) (_ bv50 6) (select a1025 (_ bv51 6))) (_ bv51 6) (select a1025 (_ bv52 6))) (_ bv52 6) (select a1025 (_ bv53 6))) (_ bv53 6) (select a1025 (_ bv54 6))) (_ bv54 6) (select a1025 (_ bv55 6))) (_ bv55 6) (select a1025 (_ bv56 6))) (_ bv56 6) (select a1025 (_ bv57 6))) (_ bv57 6) (select a1025 (_ bv58 6))) (_ bv58 6) (select a1025 (_ bv59 6))) (_ bv59 6) (select a1025 (_ bv60 6))) (_ bv60 6) (select a1025 (_ bv61 6))) (_ bv61 6) (select a1025 (_ bv62 6)))) a1025) a1025) a1277) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_4) deqeue_4)) (select a1025 head_fs_4) data_out_fs_4) data_out_fs_4) data_out_fs_4) data_out_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_2 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 6) tail_fs_4) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_4)) empty_fs_4) (_ bv1 1)) empty_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_5 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv62 6) tail_fs_4) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_4)) full_fs_4) (_ bv0 1)) full_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_0 (ite ?v_1 (ite ?v_2 (ite ?v_7 tail_fs_4 (bvadd (_ bv1 6) tail_fs_4)) (ite (= (_ bv1 1) empty_fs_4) tail_fs_4 (bvadd (_ bv63 6) tail_fs_4))) tail_fs_4) (_ bv0 6)) tail_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 6) head_fs_5) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand (bvand (bvnot (bvand (bvand (bvand (bvand (bvnot (ite (= a88 a1277) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a305 a1277) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a539 a1277) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a779 a1277) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a1025 a1277) (_ bv1 1) (_ bv0 1))))) (bvnot (bvand (bvand (bvand (bvand (bvnot (ite (= a89 a1287) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a307 a1287) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a543 a1287) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a785 a1287) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a1033 a1287) (_ bv1 1) (_ bv0 1)))))) (bvnot (bvand (bvand (bvand (bvand (bvnot (ite (= ?v_17 ?v_8) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= ?v_19 ?v_8) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= ?v_20 ?v_8) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= ?v_21 ?v_8) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= ?v_18 ?v_8) (_ bv1 1) (_ bv0 1))))))) (bvand (bvnot (bvand reset_4 (bvnot (bvand (ite (= data_out_fs_4 data_out_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_4 full_fq_4) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_4 empty_fq_4) (_ bv1 1) (_ bv0 1))))))) (bvand reset_4 (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_11 (ite ?v_12 a785 (store a785 tail_fq_3 data_in_3)) a785) a785) a785) a1033) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_3) deqeue_3)) (select a785 head_fq_3) data_out_fq_3) data_out_fq_3) data_out_fq_3) data_out_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_11 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_3 ?v_15) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_3)) empty_fq_3) (_ bv1 1)) empty_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_14 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_3 (bvadd (_ bv1 6) ?v_13)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_3)) full_fq_3) (_ bv0 1)) full_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_11 (ite ?v_12 tail_fq_3 ?v_13) tail_fq_3) tail_fq_3) (_ bv0 6)) tail_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_14 (ite (= (_ bv1 1) empty_fq_3) head_fq_3 ?v_15) head_fq_3) head_fq_3) (_ bv0 6)) head_fq_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_11 (ite ?v_16 a779 (store a779 tail_fs_3 data_in_3)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a779 (_ bv0 6) (select a779 (_ bv1 6))) (_ bv1 6) (select a779 (_ bv2 6))) (_ bv2 6) (select a779 (_ bv3 6))) (_ bv3 6) (select a779 (_ bv4 6))) (_ bv4 6) (select a779 (_ bv5 6))) (_ bv5 6) (select a779 (_ bv6 6))) (_ bv6 6) (select a779 (_ bv7 6))) (_ bv7 6) (select a779 (_ bv8 6))) (_ bv8 6) (select a779 (_ bv9 6))) (_ bv9 6) (select a779 (_ bv10 6))) (_ bv10 6) (select a779 (_ bv11 6))) (_ bv11 6) (select a779 (_ bv12 6))) (_ bv12 6) (select a779 (_ bv13 6))) (_ bv13 6) (select a779 (_ bv14 6))) (_ bv14 6) (select a779 (_ bv15 6))) (_ bv15 6) (select a779 (_ bv16 6))) (_ bv16 6) (select a779 (_ bv17 6))) (_ bv17 6) (select a779 (_ bv18 6))) (_ bv18 6) (select a779 (_ bv19 6))) (_ bv19 6) (select a779 (_ bv20 6))) (_ bv20 6) (select a779 (_ bv21 6))) (_ bv21 6) (select a779 (_ bv22 6))) (_ bv22 6) (select a779 (_ bv23 6))) (_ bv23 6) (select a779 (_ bv24 6))) (_ bv24 6) (select a779 (_ bv25 6))) (_ bv25 6) (select a779 (_ bv26 6))) (_ bv26 6) (select a779 (_ bv27 6))) (_ bv27 6) (select a779 (_ bv28 6))) (_ bv28 6) (select a779 (_ bv29 6))) (_ bv29 6) (select a779 (_ bv30 6))) (_ bv30 6) (select a779 (_ bv31 6))) (_ bv31 6) (select a779 (_ bv32 6))) (_ bv32 6) (select a779 (_ bv33 6))) (_ bv33 6) (select a779 (_ bv34 6))) (_ bv34 6) (select a779 (_ bv35 6))) (_ bv35 6) (select a779 (_ bv36 6))) (_ bv36 6) (select a779 (_ bv37 6))) (_ bv37 6) (select a779 (_ bv38 6))) (_ bv38 6) (select a779 (_ bv39 6))) (_ bv39 6) (select a779 (_ bv40 6))) (_ bv40 6) (select a779 (_ bv41 6))) (_ bv41 6) (select a779 (_ bv42 6))) (_ bv42 6) (select a779 (_ bv43 6))) (_ bv43 6) (select a779 (_ bv44 6))) (_ bv44 6) (select a779 (_ bv45 6))) (_ bv45 6) (select a779 (_ bv46 6))) (_ bv46 6) (select a779 (_ bv47 6))) (_ bv47 6) (select a779 (_ bv48 6))) (_ bv48 6) (select a779 (_ bv49 6))) (_ bv49 6) (select a779 (_ bv50 6))) (_ bv50 6) (select a779 (_ bv51 6))) (_ bv51 6) (select a779 (_ bv52 6))) (_ bv52 6) (select a779 (_ bv53 6))) (_ bv53 6) (select a779 (_ bv54 6))) (_ bv54 6) (select a779 (_ bv55 6))) (_ bv55 6) (select a779 (_ bv56 6))) (_ bv56 6) (select a779 (_ bv57 6))) (_ bv57 6) (select a779 (_ bv58 6))) (_ bv58 6) (select a779 (_ bv59 6))) (_ bv59 6) (select a779 (_ bv60 6))) (_ bv60 6) (select a779 (_ bv61 6))) (_ bv61 6) (select a779 (_ bv62 6)))) a779) a779) a1025) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_3) deqeue_3)) (select a779 head_fs_3) data_out_fs_3) data_out_fs_3) data_out_fs_3) data_out_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_11 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 6) tail_fs_3) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_3)) empty_fs_3) (_ bv1 1)) empty_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_14 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv62 6) tail_fs_3) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_3)) full_fs_3) (_ bv0 1)) full_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_9 (ite ?v_10 (ite ?v_11 (ite ?v_16 tail_fs_3 (bvadd (_ bv1 6) tail_fs_3)) (ite (= (_ bv1 1) empty_fs_3) tail_fs_3 (bvadd (_ bv63 6) tail_fs_3))) tail_fs_3) (_ bv0 6)) tail_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 6) head_fs_4) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand (bvand (bvnot (bvand (bvand (bvand (bvnot (ite (= a88 a1025) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a305 a1025) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a539 a1025) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a779 a1025) (_ bv1 1) (_ bv0 1))))) (bvnot (bvand (bvand (bvand (bvnot (ite (= a89 a1033) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a307 a1033) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a543 a1033) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a785 a1033) (_ bv1 1) (_ bv0 1)))))) (bvnot (bvand (bvand (bvand (bvnot (ite (= ?v_17 ?v_18) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= ?v_19 ?v_18) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= ?v_20 ?v_18) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= ?v_21 ?v_18) (_ bv1 1) (_ bv0 1))))))) (bvand (bvnot (bvand reset_3 (bvnot (bvand (ite (= data_out_fs_3 data_out_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_3 full_fq_3) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_3 empty_fq_3) (_ bv1 1) (_ bv0 1))))))) (bvand reset_3 (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_24 (ite ?v_25 a543 (store a543 tail_fq_2 data_in_2)) a543) a543) a543) a785) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_2) deqeue_2)) (select a543 head_fq_2) data_out_fq_2) data_out_fq_2) data_out_fq_2) data_out_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_24 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_2 ?v_28) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_2)) empty_fq_2) (_ bv1 1)) empty_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_27 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_2 (bvadd (_ bv1 6) ?v_26)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_2)) full_fq_2) (_ bv0 1)) full_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_24 (ite ?v_25 tail_fq_2 ?v_26) tail_fq_2) tail_fq_2) (_ bv0 6)) tail_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_27 (ite (= (_ bv1 1) empty_fq_2) head_fq_2 ?v_28) head_fq_2) head_fq_2) (_ bv0 6)) head_fq_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_24 (ite ?v_29 a539 (store a539 tail_fs_2 data_in_2)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a539 (_ bv0 6) (select a539 (_ bv1 6))) (_ bv1 6) (select a539 (_ bv2 6))) (_ bv2 6) (select a539 (_ bv3 6))) (_ bv3 6) (select a539 (_ bv4 6))) (_ bv4 6) (select a539 (_ bv5 6))) (_ bv5 6) (select a539 (_ bv6 6))) (_ bv6 6) (select a539 (_ bv7 6))) (_ bv7 6) (select a539 (_ bv8 6))) (_ bv8 6) (select a539 (_ bv9 6))) (_ bv9 6) (select a539 (_ bv10 6))) (_ bv10 6) (select a539 (_ bv11 6))) (_ bv11 6) (select a539 (_ bv12 6))) (_ bv12 6) (select a539 (_ bv13 6))) (_ bv13 6) (select a539 (_ bv14 6))) (_ bv14 6) (select a539 (_ bv15 6))) (_ bv15 6) (select a539 (_ bv16 6))) (_ bv16 6) (select a539 (_ bv17 6))) (_ bv17 6) (select a539 (_ bv18 6))) (_ bv18 6) (select a539 (_ bv19 6))) (_ bv19 6) (select a539 (_ bv20 6))) (_ bv20 6) (select a539 (_ bv21 6))) (_ bv21 6) (select a539 (_ bv22 6))) (_ bv22 6) (select a539 (_ bv23 6))) (_ bv23 6) (select a539 (_ bv24 6))) (_ bv24 6) (select a539 (_ bv25 6))) (_ bv25 6) (select a539 (_ bv26 6))) (_ bv26 6) (select a539 (_ bv27 6))) (_ bv27 6) (select a539 (_ bv28 6))) (_ bv28 6) (select a539 (_ bv29 6))) (_ bv29 6) (select a539 (_ bv30 6))) (_ bv30 6) (select a539 (_ bv31 6))) (_ bv31 6) (select a539 (_ bv32 6))) (_ bv32 6) (select a539 (_ bv33 6))) (_ bv33 6) (select a539 (_ bv34 6))) (_ bv34 6) (select a539 (_ bv35 6))) (_ bv35 6) (select a539 (_ bv36 6))) (_ bv36 6) (select a539 (_ bv37 6))) (_ bv37 6) (select a539 (_ bv38 6))) (_ bv38 6) (select a539 (_ bv39 6))) (_ bv39 6) (select a539 (_ bv40 6))) (_ bv40 6) (select a539 (_ bv41 6))) (_ bv41 6) (select a539 (_ bv42 6))) (_ bv42 6) (select a539 (_ bv43 6))) (_ bv43 6) (select a539 (_ bv44 6))) (_ bv44 6) (select a539 (_ bv45 6))) (_ bv45 6) (select a539 (_ bv46 6))) (_ bv46 6) (select a539 (_ bv47 6))) (_ bv47 6) (select a539 (_ bv48 6))) (_ bv48 6) (select a539 (_ bv49 6))) (_ bv49 6) (select a539 (_ bv50 6))) (_ bv50 6) (select a539 (_ bv51 6))) (_ bv51 6) (select a539 (_ bv52 6))) (_ bv52 6) (select a539 (_ bv53 6))) (_ bv53 6) (select a539 (_ bv54 6))) (_ bv54 6) (select a539 (_ bv55 6))) (_ bv55 6) (select a539 (_ bv56 6))) (_ bv56 6) (select a539 (_ bv57 6))) (_ bv57 6) (select a539 (_ bv58 6))) (_ bv58 6) (select a539 (_ bv59 6))) (_ bv59 6) (select a539 (_ bv60 6))) (_ bv60 6) (select a539 (_ bv61 6))) (_ bv61 6) (select a539 (_ bv62 6)))) a539) a539) a779) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_2) deqeue_2)) (select a539 head_fs_2) data_out_fs_2) data_out_fs_2) data_out_fs_2) data_out_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_24 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 6) tail_fs_2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_2)) empty_fs_2) (_ bv1 1)) empty_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_27 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv62 6) tail_fs_2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_2)) full_fs_2) (_ bv0 1)) full_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_22 (ite ?v_23 (ite ?v_24 (ite ?v_29 tail_fs_2 (bvadd (_ bv1 6) tail_fs_2)) (ite (= (_ bv1 1) empty_fs_2) tail_fs_2 (bvadd (_ bv63 6) tail_fs_2))) tail_fs_2) (_ bv0 6)) tail_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 6) head_fs_3) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand (bvand (bvnot (bvand (bvand (bvnot (ite (= a88 a779) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a305 a779) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a539 a779) (_ bv1 1) (_ bv0 1))))) (bvnot (bvand (bvand (bvnot (ite (= a89 a785) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a307 a785) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= a543 a785) (_ bv1 1) (_ bv0 1)))))) (bvnot (bvand (bvand (bvnot (ite (= ?v_17 ?v_21) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= ?v_19 ?v_21) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= ?v_20 ?v_21) (_ bv1 1) (_ bv0 1))))))) (bvand (bvnot (bvand reset_2 (bvnot (bvand (ite (= data_out_fs_2 data_out_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_2 full_fq_2) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_2 empty_fq_2) (_ bv1 1) (_ bv0 1))))))) (bvand reset_2 (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_32 (ite ?v_33 a307 (store a307 tail_fq_1 data_in_1)) a307) a307) a307) a543) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_1) deqeue_1)) (select a307 head_fq_1) data_out_fq_1) data_out_fq_1) data_out_fq_1) data_out_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_32 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_1 ?v_36) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_1)) empty_fq_1) (_ bv1 1)) empty_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_35 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_1 (bvadd (_ bv1 6) ?v_34)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_1)) full_fq_1) (_ bv0 1)) full_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_32 (ite ?v_33 tail_fq_1 ?v_34) tail_fq_1) tail_fq_1) (_ bv0 6)) tail_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_35 (ite (= (_ bv1 1) empty_fq_1) head_fq_1 ?v_36) head_fq_1) head_fq_1) (_ bv0 6)) head_fq_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_32 (ite ?v_37 a305 (store a305 tail_fs_1 data_in_1)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a305 (_ bv0 6) (select a305 (_ bv1 6))) (_ bv1 6) (select a305 (_ bv2 6))) (_ bv2 6) (select a305 (_ bv3 6))) (_ bv3 6) (select a305 (_ bv4 6))) (_ bv4 6) (select a305 (_ bv5 6))) (_ bv5 6) (select a305 (_ bv6 6))) (_ bv6 6) (select a305 (_ bv7 6))) (_ bv7 6) (select a305 (_ bv8 6))) (_ bv8 6) (select a305 (_ bv9 6))) (_ bv9 6) (select a305 (_ bv10 6))) (_ bv10 6) (select a305 (_ bv11 6))) (_ bv11 6) (select a305 (_ bv12 6))) (_ bv12 6) (select a305 (_ bv13 6))) (_ bv13 6) (select a305 (_ bv14 6))) (_ bv14 6) (select a305 (_ bv15 6))) (_ bv15 6) (select a305 (_ bv16 6))) (_ bv16 6) (select a305 (_ bv17 6))) (_ bv17 6) (select a305 (_ bv18 6))) (_ bv18 6) (select a305 (_ bv19 6))) (_ bv19 6) (select a305 (_ bv20 6))) (_ bv20 6) (select a305 (_ bv21 6))) (_ bv21 6) (select a305 (_ bv22 6))) (_ bv22 6) (select a305 (_ bv23 6))) (_ bv23 6) (select a305 (_ bv24 6))) (_ bv24 6) (select a305 (_ bv25 6))) (_ bv25 6) (select a305 (_ bv26 6))) (_ bv26 6) (select a305 (_ bv27 6))) (_ bv27 6) (select a305 (_ bv28 6))) (_ bv28 6) (select a305 (_ bv29 6))) (_ bv29 6) (select a305 (_ bv30 6))) (_ bv30 6) (select a305 (_ bv31 6))) (_ bv31 6) (select a305 (_ bv32 6))) (_ bv32 6) (select a305 (_ bv33 6))) (_ bv33 6) (select a305 (_ bv34 6))) (_ bv34 6) (select a305 (_ bv35 6))) (_ bv35 6) (select a305 (_ bv36 6))) (_ bv36 6) (select a305 (_ bv37 6))) (_ bv37 6) (select a305 (_ bv38 6))) (_ bv38 6) (select a305 (_ bv39 6))) (_ bv39 6) (select a305 (_ bv40 6))) (_ bv40 6) (select a305 (_ bv41 6))) (_ bv41 6) (select a305 (_ bv42 6))) (_ bv42 6) (select a305 (_ bv43 6))) (_ bv43 6) (select a305 (_ bv44 6))) (_ bv44 6) (select a305 (_ bv45 6))) (_ bv45 6) (select a305 (_ bv46 6))) (_ bv46 6) (select a305 (_ bv47 6))) (_ bv47 6) (select a305 (_ bv48 6))) (_ bv48 6) (select a305 (_ bv49 6))) (_ bv49 6) (select a305 (_ bv50 6))) (_ bv50 6) (select a305 (_ bv51 6))) (_ bv51 6) (select a305 (_ bv52 6))) (_ bv52 6) (select a305 (_ bv53 6))) (_ bv53 6) (select a305 (_ bv54 6))) (_ bv54 6) (select a305 (_ bv55 6))) (_ bv55 6) (select a305 (_ bv56 6))) (_ bv56 6) (select a305 (_ bv57 6))) (_ bv57 6) (select a305 (_ bv58 6))) (_ bv58 6) (select a305 (_ bv59 6))) (_ bv59 6) (select a305 (_ bv60 6))) (_ bv60 6) (select a305 (_ bv61 6))) (_ bv61 6) (select a305 (_ bv62 6)))) a305) a305) a539) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_1) deqeue_1)) (select a305 head_fs_1) data_out_fs_1) data_out_fs_1) data_out_fs_1) data_out_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_32 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 6) tail_fs_1) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_1)) empty_fs_1) (_ bv1 1)) empty_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_35 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv62 6) tail_fs_1) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_1)) full_fs_1) (_ bv0 1)) full_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_30 (ite ?v_31 (ite ?v_32 (ite ?v_37 tail_fs_1 (bvadd (_ bv1 6) tail_fs_1)) (ite (= (_ bv1 1) empty_fs_1) tail_fs_1 (bvadd (_ bv63 6) tail_fs_1))) tail_fs_1) (_ bv0 6)) tail_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 6) head_fs_2) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand (bvand (bvnot (bvand (bvnot (ite (= a88 a539) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a305 a539) (_ bv1 1) (_ bv0 1))))) (bvnot (bvand (bvnot (ite (= a89 a543) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= a307 a543) (_ bv1 1) (_ bv0 1)))))) (bvnot (bvand (bvnot (ite (= ?v_17 ?v_20) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= ?v_19 ?v_20) (_ bv1 1) (_ bv0 1))))))) (bvand (bvnot (bvand reset_1 (bvnot (bvand (ite (= data_out_fs_1 data_out_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_1 full_fq_1) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_1 empty_fq_1) (_ bv1 1) (_ bv0 1))))))) (bvand reset_1 (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_40 (ite ?v_41 a89 (store a89 tail_fq_0 data_in_0)) a89) a89) a89) a307) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite (= (_ bv1 1) (bvand (bvnot empty_fq_0) deqeue_0)) (select a89 head_fq_0) data_out_fq_0) data_out_fq_0) data_out_fq_0) data_out_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_40 (_ bv0 1) (ite (= (_ bv1 1) (ite (= tail_fq_0 ?v_44) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fq_0)) empty_fq_0) (_ bv1 1)) empty_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_43 (_ bv0 1) (ite (= (_ bv1 1) (ite (= head_fq_0 (bvadd (_ bv1 6) ?v_42)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fq_0)) full_fq_0) (_ bv0 1)) full_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_40 (ite ?v_41 tail_fq_0 ?v_42) tail_fq_0) tail_fq_0) (_ bv0 6)) tail_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_43 (ite (= (_ bv1 1) empty_fq_0) head_fq_0 ?v_44) head_fq_0) head_fq_0) (_ bv0 6)) head_fq_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_40 (ite ?v_45 a88 (store a88 tail_fs_0 data_in_0)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store a88 (_ bv0 6) (select a88 (_ bv1 6))) (_ bv1 6) (select a88 (_ bv2 6))) (_ bv2 6) (select a88 (_ bv3 6))) (_ bv3 6) (select a88 (_ bv4 6))) (_ bv4 6) (select a88 (_ bv5 6))) (_ bv5 6) (select a88 (_ bv6 6))) (_ bv6 6) (select a88 (_ bv7 6))) (_ bv7 6) (select a88 (_ bv8 6))) (_ bv8 6) (select a88 (_ bv9 6))) (_ bv9 6) (select a88 (_ bv10 6))) (_ bv10 6) (select a88 (_ bv11 6))) (_ bv11 6) (select a88 (_ bv12 6))) (_ bv12 6) (select a88 (_ bv13 6))) (_ bv13 6) (select a88 (_ bv14 6))) (_ bv14 6) (select a88 (_ bv15 6))) (_ bv15 6) (select a88 (_ bv16 6))) (_ bv16 6) (select a88 (_ bv17 6))) (_ bv17 6) (select a88 (_ bv18 6))) (_ bv18 6) (select a88 (_ bv19 6))) (_ bv19 6) (select a88 (_ bv20 6))) (_ bv20 6) (select a88 (_ bv21 6))) (_ bv21 6) (select a88 (_ bv22 6))) (_ bv22 6) (select a88 (_ bv23 6))) (_ bv23 6) (select a88 (_ bv24 6))) (_ bv24 6) (select a88 (_ bv25 6))) (_ bv25 6) (select a88 (_ bv26 6))) (_ bv26 6) (select a88 (_ bv27 6))) (_ bv27 6) (select a88 (_ bv28 6))) (_ bv28 6) (select a88 (_ bv29 6))) (_ bv29 6) (select a88 (_ bv30 6))) (_ bv30 6) (select a88 (_ bv31 6))) (_ bv31 6) (select a88 (_ bv32 6))) (_ bv32 6) (select a88 (_ bv33 6))) (_ bv33 6) (select a88 (_ bv34 6))) (_ bv34 6) (select a88 (_ bv35 6))) (_ bv35 6) (select a88 (_ bv36 6))) (_ bv36 6) (select a88 (_ bv37 6))) (_ bv37 6) (select a88 (_ bv38 6))) (_ bv38 6) (select a88 (_ bv39 6))) (_ bv39 6) (select a88 (_ bv40 6))) (_ bv40 6) (select a88 (_ bv41 6))) (_ bv41 6) (select a88 (_ bv42 6))) (_ bv42 6) (select a88 (_ bv43 6))) (_ bv43 6) (select a88 (_ bv44 6))) (_ bv44 6) (select a88 (_ bv45 6))) (_ bv45 6) (select a88 (_ bv46 6))) (_ bv46 6) (select a88 (_ bv47 6))) (_ bv47 6) (select a88 (_ bv48 6))) (_ bv48 6) (select a88 (_ bv49 6))) (_ bv49 6) (select a88 (_ bv50 6))) (_ bv50 6) (select a88 (_ bv51 6))) (_ bv51 6) (select a88 (_ bv52 6))) (_ bv52 6) (select a88 (_ bv53 6))) (_ bv53 6) (select a88 (_ bv54 6))) (_ bv54 6) (select a88 (_ bv55 6))) (_ bv55 6) (select a88 (_ bv56 6))) (_ bv56 6) (select a88 (_ bv57 6))) (_ bv57 6) (select a88 (_ bv58 6))) (_ bv58 6) (select a88 (_ bv59 6))) (_ bv59 6) (select a88 (_ bv60 6))) (_ bv60 6) (select a88 (_ bv61 6))) (_ bv61 6) (select a88 (_ bv62 6)))) a88) a88) a305) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite (= (_ bv1 1) (bvand (bvnot empty_fs_0) deqeue_0)) (select a88 head_fs_0) data_out_fs_0) data_out_fs_0) data_out_fs_0) data_out_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_40 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv1 6) tail_fs_0) (_ bv1 1) (_ bv0 1))) (_ bv1 1) empty_fs_0)) empty_fs_0) (_ bv1 1)) empty_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_43 (_ bv0 1) (ite (= (_ bv1 1) (ite (= (_ bv62 6) tail_fs_0) (_ bv1 1) (_ bv0 1))) (_ bv1 1) full_fs_0)) full_fs_0) (_ bv0 1)) full_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (ite ?v_38 (ite ?v_39 (ite ?v_40 (ite ?v_45 tail_fs_0 (bvadd (_ bv1 6) tail_fs_0)) (ite (= (_ bv1 1) empty_fs_0) tail_fs_0 (bvadd (_ bv63 6) tail_fs_0))) tail_fs_0) (_ bv0 6)) tail_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (ite (= (_ bv0 6) head_fs_1) (_ bv1 1) (_ bv0 1)) (bvand (bvnot (bvand reset_0 (bvnot (bvand (ite (= data_out_fs_0 data_out_fq_0) (_ bv1 1) (_ bv0 1)) (bvand (ite (= full_fs_0 full_fq_0) (_ bv1 1) (_ bv0 1)) (ite (= empty_fs_0 empty_fq_0) (_ bv1 1) (_ bv0 1))))))) (bvnot (bvand (bvand (ite (= a88 a305) (_ bv1 1) (_ bv0 1)) (ite (= a89 a307) (_ bv1 1) (_ bv0 1))) (ite (= ?v_17 ?v_19) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (_ bv0 1)))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
